i:Id, p:finite-prob-space, ds:fpf(Id; x.Type), P:(decl-state(ds)).
normal-ds{i:l}
normal-ds(ds)
 es-real{i:l}
 es-real(es.@i Precondition for mkid{a:ut2}(Outcome(p)) P discrete state(ds)) 

latex

Definitions

True, T, guard(T), sq_type(T), A, P  Q, existse-ge(es; e; e'.P(e')), x. t(x), prop{i:l}, alle-at(es; i; e.P(e)), A c B, P  Q, R-realizes{i:l}(R; es.P(es)), x:A. B(x), t  T, mkid{$x:ut2}, @i Precondition for a(Outcome(p)) P discrete state(ds), es-real{i:l}(es.P(es)), P  Q, Id, x:A. B(x), False, decidable(P), x(s), pre-p(es; i; ds; a; p; P)

Lemmas

dds-init-elapsed, dds-state-after-elapsed, true wf, squash wf, es-le wf, rationals wf, es-le-loc, Id sq, es-state-after wf, not wf, decidable equal Kind, finite-prob-space wf, fpf wf, bool wf, decl-state wf, normal-ds wf, discrete-pre-p wf, R-realizes wf, event system wf, R-consistent wf, es-dds wf, es-state-subtype2, es-init-state wf, assert wf, es-E wf, es-loc wf, Id wf, locl wf, es-kind wf, Knd wf, pre-p-realizable